…made the translation of bitvector permissions to just be bitvectors

…-irts

…pes with no return value

… be converted to unit, not to the empty struct

…tly to the expected LLVM type

…a HeapsterEnv into a single function which iterates through the globals and adds those it can handle

…y types for it

…enerated LLVM files

…macro, because that seems to be the proper way to do things

…rences into one

…issions

…ons with different fields using the SImpl_LLVMArrayContents rule; to get the translation of the SImpl_LLVMArrayContents to work correctly, I had to change local implications to not use strict tuples, which in turn required changing the translation of lowned permissions (which are themselves local implications) to not use strict tuples as well

… prover can map array permission contents

…sion syntax

…-conjunctive permissions returned by implElimLLVMBlock; added pretty-printing and typing information for the names bound by local implications

… of defined permissions

…e local implication used to prove array contents!

…nerate the sub-array being borrowed, and to only take the borrows from the larger array that could overlap with the sub-array; Added cases to prove field permissions from arrays of smaller strides; added more debug information

…t from the sub-array instead of those the could overlap with it

… a tag first, thereby reducing the cases in which they bottom out into general disjunctions

…tImplBlock delete all the BVRanges of perms on the left-hand size from the BVRange of the right-hande side, and then creating blocks with existentially-quantified shapes for those ranges

…lockPermToField and llvmBlockPermToArray, because these do not take the current partial substitution into account

…ng the recent merge

…example that no longer work